package automatica;

import static org.w3c.dom.Node.ELEMENT_NODE;




import java.io.File;
import java.io.IOException;
import java.net.MalformedURLException;
import java.net.URL;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.Random;
import java.util.Vector;
import java.util.Map.Entry;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

import javax.swing.JFrame;
import javax.swing.JOptionPane;

import org.jdesktop.jdic.browser.WebBrowser;
import org.jgrapht.DirectedGraph;
import org.jgrapht.alg.CycleDetector;
import org.jgrapht.graph.DefaultDirectedGraph;
import org.jgrapht.graph.DefaultEdge;
import org.w3c.dom.Attr;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
import org.w3c.dom.NamedNodeMap;
import org.w3c.dom.Node;
import org.w3c.dom.NodeList;

import automatica.NLParser.Corpus;
import automatica.NLParser.PhraseParser;
import net.sf.saxon.s9api.SaxonApiException;
import prefuse.data.Graph;
import prefuse.data.Table;

/**
 * @author Xiaoyu E-mail: franknewchen@gamil.com
 * @version 创建时间：2012-9-5 上午10:58:02
 * 类说明
 */

/**
 * @author franknewchen
 *
 */
public class Utility {

	/*
	 * get the type of a concept according to the definition
	 * the defBody may contain several return instances, so the result is a vector
	 */
	public static Vector<Type> getReturnTypesOfDefbody(String defBody, GSI gsi, String dataType){
		Vector<Type> result = new Vector<Type>(1,1);
		if(dataType.indexOf("Definition")!=-1&&dataType.indexOf("Formal")!=-1&&dataType.indexOf("String")!=-1){
		if(defBody!=null&&defBody!=""){
			Vector<String> binding = Utility.splitAllList(defBody);
			for(int i = 0; i < binding.size(); i++){
				Vector<String> oc = Utility.splitBinding(binding.get(i));
				String fatherInstance = oc.get(0);
				System.out.println("Farther instance: " + fatherInstance);	
				result.add(new Type(fatherInstance,gsi));
			}

		}
		}
		
		return result;
	}
	
	/*
	 * ÔÚindexÖÐÆ¥Åätype
	 * ·µ»ØËùÓÐÆ¥ÅäµÄ¶¨ÒåÔÚindexÖÐµÄÐÐºÅ£¬×¢ÒâÕâÀïÆ¥ÅäÊµÔÚauthor contextµÄÒâÒåÏÂµÄ
	 * 解决不同用户的问题
	 */
	public static Vector<Integer> matchDefinitionFromIndex(Type type, TypeIndex index){
		Vector<Integer> result = new Vector<Integer>(1,1);
			for(int j = 0; j < index.getRowCount(); j++){
				//vocabulary + pattern   n-->1  type  1-->n  definition
				if(index.getString(j, "childType").equals(type.getValue())){
					result.add(j);
				}
			}
		
		return result;
	}
	
	
	
	/**
	 * 
	 * type ÖÐÖ»°üº¬conceptObjectµÄº¯Êý£¬¶ø²»°üº¬ÏµÍ³ÄÚ½¨µÄ´úÊý£¬Âß¼­£¬ÒÔ¼°¼¯ºÏÔËËãµÄº¯Êý£¬ºÍÁÐ±í
	 * @param type
	 * @param index
	 * @return
	 */
	public static Vector<Node> fetchDefinitionNodeFromIndex(Type type, TypeIndex index){
		Vector<Node> result = new Vector<Node>(1,1);
		Vector<Integer> defs = new Vector<Integer>(1,1);
		//System.out.println(type);
		defs = matchDefinitionFromIndex(type, index);
		if(type.isPolishType()){
			if(defs.size()<=0){
				//Ôò½øÐÐÀàÐÍÌáÉý
				Vector<String> termSet = Utility.generateTermSet(type.getValue());
				if(termSet.size()>1){
					Vector[] data = new Vector[termSet.size()-1]; 
					StringBuffer newType = new StringBuffer();
					//µ±ÀàÐÍÖÐÓÐ¡°{}¡±¿ÉÒÔºöÂÔ£¬ÒòÎªÁÐ±íÔÚÇóÀàÐÍÖ®Ç°¾Í±»´¦ÀíÁË
					if(type.getValue().indexOf("{")!=-1){
						//if(Utility.isInStringArray(type.getValue(), constants.GTextbookConstants.conceptThatEliminateList)){
							//if it is "collinear" "collinearLine" "line", then eliminate "{""}"
						if(Utility.isPolishFormula(type.getValue())){
							if(termSet.size()==2&&Utility.isList(termSet.get(1))){
								System.out.println(type.getValue());
								result = fetchDefinitionNodeFromIndex(new Type(type.getValue().replaceAll("\\{", "").replaceAll("\\}", "").replaceAll(";", ",")),index);
							}
						}else{
							//Èç¹ûÊôÐÔÊÇÁÐ±í£¬ÔòÈ¡ÆäÒ»¸ömidpoint({A1,B1,C1},{A2,B2,C2}) --> midpoint(A1,B1)
							Vector[] items = new Vector[termSet.size()-1];
							for(int j = 1 ; j < termSet.size(); j++){
								items[j-1] = Utility.splitAllList(termSet.get(j));
							}
							newType.append(termSet.get(0)+"(");

							for(int k = 0 ; k < termSet.size()-1; k++){
								newType.append(items[k].get(0)+",");
							}
							newType.replace(newType.lastIndexOf(","),newType.length(),")");
	
							result = fetchDefinitionNodeFromIndex(new Type(newType.toString()),index);
							
						}
					}else{
						for(int i = 1; i<termSet.size(); i++){			
							data[i-1] = new Type(termSet.get(i)).getFatherTypesFromIndex(index);
							data[i-1].add(termSet.get(i)); 
						}
						
						Vector<String> attriList = Type.generateCombinationList(data);
						for(int j = 0; j < attriList.size(); j++){		
							StringBuffer buffer = new StringBuffer();
							buffer.append(termSet.get(0)).append("(").append(attriList.get(j)).append(")");
							if(buffer.indexOf("{")!=-1){
								result.addAll(fetchDefinitionNodeFromIndex(new Type(buffer.toString()),index));
							}
							//check and get the father type by definition, then getFatherTypes of the new type
							defs = matchDefinitionFromIndex(new Type(buffer.toString()), index);
							if(defs.size()>0 || result.size()>0){
								break;
							}
						}
					
					}
				}
				
				for(int t = 0; t < defs.size(); t++){
					String v = type.getValue();
					if(v.indexOf("(Circle)")==-1&&v.indexOf("(Line)")==-1&&v.indexOf("Segment")==-1){
						index.addRow();
						int size = index.getRowCount();
						index.setString(size-1, "childType", type.getValue());
						index.setString(size-1, "fatherType", index.getString(defs.get(t), "childType"));
						index.setInt(size-1, "id", index.getInt(defs.get(t), "id"));
						index.setString(size-1, "username", index.getString(defs.get(t), "username"));
						index.setString(size-1,"version",index.getString(defs.get(t), "version"));
						System.out.println(index.getString(size-1, "childType") + "------->>>>" +index.getString(size-1, "fatherType"));
						index.print();
					}
				}
				
				
			}
		}
		
		
		for(int t = 0; t < defs.size(); t++){
			Document script = index.getScriptDoc();
			Element root = script.getDocumentElement();
			result.add(Utility.getChildById(root, index.getInt(defs.get(t), "id"), ELEMENT_NODE));
		}
		
		
		return result;
	}
	

	/**
	 * ¶¨ÒåÐÎÊ½Ä£Ê½µÄ·ÖÀàÌåÏµ
	 * isStatement
	 * 		isConfiguration
	 * 		isAssumption
	 * 		isObjective
	 * 		isDeclaration
	 * 		isGiveClause
	 * isList 
	 * isLogicalFormula
	 * 		isPolishLogicalFormula
	 * 		isConventionalLogicalFormula
	 * isClause
	 * 		isReference
	 * 		isBinding
	 * isPolishFormula È«²¿Îª´øÀ¨ºÅµÄ¹«Ê½
	 * 		isPolishGeometricFormula -- not isPolishAlgebraicFormula and isPolishFormula
	 * 		isPolishAlgebraicFormula -- quantityFunction
	 * 			sin(),cos()
	 * isConventionalFormula ·ûºÅÓëÀ¨ºÅ»ìºÏµÄ¹«Ê½
	 * 		isConventionalGeometricFormula -- º¬ÓÐÄÇÐ©·ûºÅ
	 * 		isConventionalAlgebraicFormula -- º¬ÓÐÄÇÐ©·ûºÅ
	 * isMathematicalFormula
	 * 		isPolishFormula
	 * 		isConventionalFormula
	 * isAlgebraicFormula
	 * 		isPolishAlgebraicFormula
	 * 		isConventionalAlgebraicFormula
	 * isGeometricFormula
	 * 		isConventionalGeometricFormula
	 * 		isPolishGeometricFormula
	 * isNumeric
	 * isAbstractInstance
	 * 		isQuantityOfAbstractInstance
	 * isConstant
	 * 		isDegreeConstant
	 * 
	 * isPointer
	 * 
	 * isSetOperation
	 * 
	 * 
	 * ------------------------
	 * isConcept
	 * 		isPolishGeometricFormula
	 * isReturnBody
	 * 		isBinding
	 * 		isList
	 * 		isAbstractInstance
	 * 
	 */
	
	/*
	 * check whether pattern is a function
	 * f(A,B) = c
	 * a + b = c
	 * ***************************************************************
	 * TO DO
	 * **************************************************************
	 * 
	 */
	
	
	public static boolean isConventionalGeometricFormula(String pattern){
		return false;
	}
	
	public static boolean isConventionalAlgebraicFormula(String pattern){
		return false;
	}
	
	public static boolean isPolishGeometricFormula(String pattern){
		if(isPolishFormula(pattern)&&!isPolishAlgebraicFormula(pattern))
			return true;
		else
			return false;
	}
	
	/**
	 * Ç°×ºÐÎÊ½µÄ´úÊý±í´ïÊ½
	 * @param pattern
	 * @return
	 */
	public static boolean isPolishAlgebraicFormula(String pattern){
		String buf = Utility.deleteSpace(pattern);
		if(matchReservedWords(pattern,constants.GTextbookConstants.algebraicWords)){
			return true;
		}
		else return false;
	}
	
	public static boolean isAlgebraicFormula(String pattern){
		if(isConventionalAlgebraicFormula(pattern)||isPolishAlgebraicFormula(pattern)){
			return true;
		}else 
			return false;
	}
	
	public static boolean isGeometricFormula(String pattern){
		if(isConventionalGeometricFormula(pattern)||isPolishGeometricFormula(pattern)){
			return true;
		}else 
			return false;
	}
	/**
	 * 
	 * Ç°×ºÊ½±í´ïÊ½	
	 * @param pattern
	 * @return
	 */
	public static boolean isPolishFormula(String pattern){
		if(pattern.indexOf("(")!= -1 
				&& !isClause(pattern) && !isLogicalFormula(pattern) && !isList(pattern) 
				&& !isStatement(pattern) && !isConventionalFormula(pattern)){
			return true;
		}
		else return false;
	}
	
	public static boolean isConventionalFormula(String pattern){
		if(isConventionalAlgebraicFormula(pattern)||isConventionalGeometricFormula(pattern)){
			return true;
		}else 
			return false;
	}
	
	
	public static boolean isMathematicalFormula(String pattern){
		if(isConventionalFormula(pattern)||isPolishFormula(pattern)){
			return true;
		}else 
			return false;
	}
	/**
	 * check whether str is numeric: Interger or Real
	 * @param str
	 * @return
	 */
	public static boolean isNumeric(String str){
		  //str = deleteSpace(str).replace(".", "");
		  for (int i = str.length();--i>=0;){   
		   if (!Character.isDigit(str.charAt(i))){
		    return false;
		   }
		  }
		  return true;
	}
	
	/**
	 * check whether str is a constant
	 * @param str
	 * @return
	 */
	public static boolean isConstant(String str){
		if(isDegreeConstant(str)){
			return true;
		}else
			return false;
	}
	
	public static boolean isDegreeConstant(String str){
		  str = deleteSpace(str);
		  if(str.indexOf("pi")!=-1||str.indexOf("Pi")!=-1){
			  return true;
		  }else
		  return false;
	}
	
	/*
	 * check whether pattern is an abstract instance
	 */
	public static boolean isAbstractInstance(String pattern){
		if(pattern.indexOf("::")!=-1 && !isPolishFormula(pattern) && !isClause(pattern)
				&& !isLogicalFormula(pattern)&& !isStatement(pattern)&&!isConventionalFormula(pattern)
				&& !isList(pattern)){
			return true;
		}else return false;
	}
	
	
	/*
	 * check whether test is a quantity
	 * r::length|area|degree|Length|Area|Degree|algebraicQuantity|geometricQuantity
	 * 
	 */
	public static boolean isQuantityOfAbstractInstance(String test){
		if(isAbstractInstance(test)){
			String[] a = generateAbstractTypeSet(test);
			//check the quantity type
			String type = a[1];
			if(type.equals("Length")|type.equals("Area")|type.equals("Degree")
					|type.equals("AlgebraicQuantity")|type.equals("GeometricQuantity")|type.equals("Integer")|type.equals("Decimal")){
				return true;
			}else return false;
		
		}else return false;
	}
	
	public static boolean isReference(String pattern){
		if(pattern.indexOf(":=")!=-1 && !isBinding(pattern)
				&& !isLogicalFormula(pattern)&& !isStatement(pattern))
			return true;
		else return false;
	}
	
	public static boolean isConfiguration(String pattern){
		Utility.deleteSpace(pattern);
		if(pattern.indexOf("configuration(")==0){
			return true;
		}
		else return false;
	}
	
	public static boolean isAssumption(String pattern){
		Utility.deleteSpace(pattern);
		if(pattern.indexOf("assume(")==0||pattern.indexOf("hypothesis(")==0){
			return true;
		}
		else return false;
	}
	
	public static boolean isObjective(String pattern){
		Utility.deleteSpace(pattern);
		if(pattern.indexOf("show(")==0||pattern.indexOf("objective(")==0){
			return true;
		}
		else return false;
	}
	
	public static boolean isDeclaration(String pattern){
		Utility.deleteSpace(pattern);
		if(pattern.indexOf("declare(")==0||pattern.indexOf("Declare(")==0){
			return true;
		}
		else return false;
	}
	
	public static boolean isGiveClause(String pattern){
		Utility.deleteSpace(pattern);
		if(pattern.indexOf("give(")==0||pattern.indexOf("Give(")==0){
			return true;
		}
		else return false;
	}
	
	public static boolean isPolishLogicalFormula(String pattern){
		String buf = pattern.trim();
		return matchReservedWords(buf,constants.GTextbookConstants.logicalWords);
	}
	
	public static boolean isConventionalLogicalFormula(String pattern){
		return false;
	}
	
	public static boolean isLogicalFormula(String pattern){
		if(isPolishLogicalFormula(pattern)||isConventionalLogicalFormula(pattern)){
			return true;
		}
		else return false;
	}
	
	public static boolean isSetOperation(String pattern){
		if(Utility.isInStringArray(pattern, constants.GTextbookConstants.operation4Set)){
			return true;
		}else return false;
	}
	
	/*
	 * check whether test is a list
	 */
	public static boolean isList(String test){
		String form = deleteSpace(test);
		if(form.charAt(0)=='{'&& form.charAt(form.length()-1)=='}'){
			if(isReference(form)){
				if(isList(Utility.generateReferenceSet(form)[0]))
					return false;
				else
					return true;
				
			}else return true;

		}else return false;
	}
	
	/*
	 * check whether test is a binding
	 */
	public static boolean isBinding(String test){
		if(deleteSpace(test).charAt(0)=='['){
			return true;
		}else return false;
	}
	public static boolean isClause(String pattern){
		if(isReference(pattern) || isBinding(pattern)){
			return true;
		}else
			return false;
	}
	
	public static boolean isConcept(String pattern){
		if(isPolishGeometricFormula(pattern)){
			return true;
		}else
			return false;
	}
	
	public static boolean isReturnBody(String pattern){
		if(isBinding(pattern) || isList(pattern) || isAbstractInstance(pattern)){
			return true;
		}else 
			return false;
	}
	
	public static boolean isStatement(String pattern){
		if(isConfiguration(pattern) || isAssumption(pattern) || isObjective(pattern) || isDeclaration(pattern) || isGiveClause(pattern)){
			return true;
		}else 
			return false;
	}
	
	public static boolean isEquivalence(String pattern){
		if(pattern.indexOf("<=>")!=-1){
			return true;
		}else 
			return false;
	}

	/*
	 * check whether instance is a pointer
	 */
	public static boolean isPointer(String instance){
		if(!isAbstractInstance(instance) && !isPolishFormula(instance)
				&& !isClause(instance) && !isLogicalFormula(instance) && !isList(instance) 
				&& !isStatement(instance) && !isConventionalFormula(instance) && !isNumeric(instance)&&!isConstant(instance)){
			return true;
		}else return false;
	}
	

	
	   //check whether there is vocabulary in test
	   public static boolean havePredicate(String test){
	      String reg = "\\(|\\（";
	      Pattern pattern = Pattern.compile(reg);
	      Matcher m = pattern.matcher(test);
	      if(m.find())
	      return true;
	      else
	      return false;
	   }
	
	  public static String deleteSpace(String test){
	      StringBuffer result = new StringBuffer();
	      String reg = "\\s";                        //Ö¸¶¨ÒªÉ¾³ýµÄ×Ö·û
	      Pattern pattern = Pattern.compile(reg);
	      Matcher m = pattern.matcher(test);      
	      Vector<Integer> spaceIndex = new Vector<Integer>(10,10);
	      int start = 0;
	      int end = 0;
	      while( m.find() ){
	      spaceIndex.add(m.start());                   //±ê¼ÇÒªÉ¾³ýµÄ×Ö·û
	     }
	     if(spaceIndex.isEmpty())
	      return test;
	     else{
	         for(int i = 0; i < spaceIndex.size();i++){          
	            end = spaceIndex.get(i);
	            if(start == end){
	               start = end+1;
	            if(start > test.length()-1)
	              break;
	            if(i == spaceIndex.size()-1)
	               end = test.length();
	            else{                 
	               end = spaceIndex.get(i+1);
	               continue;
	            }
	            }  
	            result.append(test.substring(start,end));
	            start = end +1;
	            if(start > test.length())
	               break;        
	         }
	         if(start <= test.length()-1){      
	        	 end = test.length();
	        	 result.append(test.substring(start,end));
	         }
	     return result.toString();
	        }
	    }
	  
	  /*
	   * have already deleted the white space
	   * parse the string of test in the form
	   * {{A;B};C}
	   * vector of A, B, C
	   */
	  public static Vector<String> splitAllList(String test){
		  Vector<String> result = new Vector<String>(1,1);
	      String reg = "\\{|\\}|\\;|\\；";                        //Ö¸¶¨ÒªÉ¾³ýµÄ×Ö·û
	      Pattern pattern = Pattern.compile(reg);
	      Matcher m = pattern.matcher(test);
	      Vector<Integer> positions = new Vector<Integer>(1,1);
	      while(m.find()){
		      positions.add(m.start());  
	      }
	      
	      if(Utility.isList(test)){
	    	  int i = 1;
	    	  while(i<positions.size()){
	    		  if(positions.get(i-1)+1 != positions.get(i)){
	    			  String buffer = test.substring(positions.get(i-1)+1,positions.get(i));
	    			  result.add(deleteSpace(buffer));
	    		  }
	    		  i++;
	    	  }
	      }else result.add(test);
		  
		  return result;
	  }
	  
	  
	  public static Vector<String> splitList(String test){
		  Vector<String> result = new Vector<String>(1,1);
	      String reg = "\\{|\\}|\\;|\\；";                        //Ö¸¶¨ÒªÉ¾³ýµÄ×Ö·û
	      Pattern pattern = Pattern.compile(reg);
	      Matcher m = pattern.matcher(test);
	      Vector<Integer> positions = new Vector<Integer>(1,1);
	      while(m.find()){
		      positions.add(m.start());  
	      }
	      
	      if(Utility.isList(test)){
	    	  int i = 1;
	    	  while(i<positions.size()){
	    		  if(positions.get(i-1)+1 != positions.get(i)){
	    			  String buffer = test.substring(positions.get(i-1)+1,positions.get(i));
	    			  result.add(deleteSpace(buffer));
	    		  }
	    		  i++;
	    	  }
	      }else result.add(test);
		  
		  return result;
	  }
	  
	  /*
	   * have already deleted the white space
	   * parse the string of test in the form 
	   * [A where B]
	   * vector of A, B
	   */
	  public static Vector<String> splitBinding(String test){
		  Vector<String> result = new Vector<String>(1,1);
	      String reg = "\\[|\\]|where|Where";                    
	      Pattern pattern = Pattern.compile(reg);
	      Matcher m = pattern.matcher(test);
	      Vector<Integer> starts = new Vector<Integer>(1,1);
	      Vector<Integer> ends = new Vector<Integer>(1,1);
	      while(m.find()){
		      starts.add(m.start());
		      ends.add(m.end());
	      }
	      
	      if(Utility.isBinding(test)){
	    	  int i = 1;
	    	  while(i<starts.size()){
	    		  String buffer = test.substring(ends.get(i-1),starts.get(i));
	    		  if(buffer!=null){
	    			  result.add(deleteSpace(buffer));
	    		  }
	    		  i++;
	    	  }
		  
	      }else result.add(test);
		  return result;
	  }
	  
	  /*
	   * have already deleted the white space
	   * parse the string of test in the form 
	   * and|or|not(clause1,clause2)
	   * vector of clause1, clause2
	   */
	  public static Vector<String> splitConstraint(String test){
		  Vector<String> result = new Vector<String>(1,1);
		  if(isLogicalFormula(test)){
			 Vector<String> tree = Utility.generateTermSet(test);
			 for(int i = 0; i < tree.size(); i++){
				result.addAll(splitConstraint(deleteSpace(tree.get(i))));
			}
		  }else{
				result.add(test);
			}
	      
		  return result;
	  }
	  
	  
	  /*
	   * have already deleted the white space
	   * parse the string of test in the form of
	   * A;B;C;D;
	   * vector of A, B, C,D
	   */
	  public static Vector<String> splitStatement(String test){
		  Vector<String> result = new Vector<String>(1,1);
	      String reg = ";";                    
	      Pattern pattern = Pattern.compile(reg);
	      Matcher m = pattern.matcher(test);
	      Vector<Integer> starts = new Vector<Integer>(1,1);
	      Vector<Integer> ends = new Vector<Integer>(1,1);
	      ends.add(0);
	      while(m.find()){
		      starts.add(m.start());
		      ends.add(m.end());
	      }
	      starts.add(test.length());
	      int i = 0;
	      while(i<starts.size()){
	    	  String buffer = test.substring(ends.get(i),starts.get(i));
	    	  if(buffer!=null){
	    		  result.add(deleteSpace(buffer));
	    	  }
	    	  i++;
	      }
		  
		  
		  return result;
	  }
	  
	  
	  /*
	   * parse the string test in the form
	   * vocabulary(term,...,term)
	   * the first place is vocabulary, the second place is (term,...,term)
	   */
	  public static String[] splitVocabularyAttribute(String test){
		  String[] result = new String[2];                 
	      int index = test.indexOf('(');
	      result[0] = test.substring(0,index);
	      result[1] = test.substring(index,test.length());

		  return result;
	  }
	  
	  
	  /*
	   * have already deleted the white space
	   * parse the string test in the form of
	   * A:=B
	   * the first place is A, the second place is B
	   */
	  public static String[] generateReferenceSet(String test){
		  String[] result = new String[2];
	      String reg = ":=";                    
	      Pattern pattern = Pattern.compile(reg);
	      Matcher m = pattern.matcher(test);
	      int start = 0;
	      while(m.find()){
	    	  String buffer = test.substring(start,m.start());
	    	  if(buffer!=null){
	    		  result[0] = deleteSpace(buffer);
	    	  }
	    	  buffer = test.substring(m.end(),test.length());
	    	  if(buffer!=null){
	    		  result[1] = deleteSpace(buffer);
	    	  }
	      }

		  return result;
	  }
	  
	  
	  /* 
	   * have already deleted the white space
	   * parse the string test in the form
	   * A::type
	   * the first place is A, the second place is type
	   */
	  public static String[] generateAbstractTypeSet(String test){
		  String[] result = new String[2];
	      String reg = "::";                    
	      Pattern pattern = Pattern.compile(reg);
	      Matcher m = pattern.matcher(test);
	      int start = 0;
	      while(m.find()){
	    	  String buffer = test.substring(start,m.start());
	    	  if(buffer!=null){
	    		  result[0] = deleteSpace(buffer);
	    	  }
	    	  buffer = test.substring(m.end(),test.length());
	    	  if(buffer!=null){
	    		  result[1] = deleteSpace(buffer);
	    	  }
	      }

		  return result;
	  }
	     
	/* 
	 * have already deleted the white space
	 * parse the test string in the form 
	 * $vocabulary$(term,term,...,term)
	 * the first place is the vocabulary and the others are the terms
	 */
	   public static Vector<String> generateTermSet(String test){
		   test = deleteSpace(test);
	      int[][] t = matchPairs(test);
	      Vector<String> term = new Vector<String>(5,5);
	      term.add(test.substring(0,t[0][0]));
	      int begin = t[0][0]+1;
	      int over = 0;
	      while(begin < test.length()){
	         for(int point = begin;point < test.length();point++){
	            if(test.charAt(point)=='('){
	               for(int y = 0;y < t.length;y++){
	                  if(t[y][0] == point)
	                    { 
	                    point = t[y][1]+1;
	                  //  System.out.println("The mark of extracted term: "+ t[y][1]);
	                    break;
	                    }
	                                          
	               }
	            }
	            if(test.charAt(point)==','||test.charAt(point)==')'){
	               over = point;
	               break;
	            }
	            
	         }  				//È·¶¨ÖÕµã
	         
	         if(begin!=over || begin > over){
	        	 term.add(test.substring(begin,over));       //ÌáÈ¡Ïî
	         }
	         begin = over+1;                                //ÖØÐÂÌáÈ¡ 
	         
	      }
	      return term;
	   }
	   
	   //À¨ºÅÅä¶Ô
	  public static int[][] matchPairs(String test){
	      Vector<Integer> textBone = new Vector<Integer>(10,10);
	      String regEx = "\\(|\\)|\\（|\\）";
	      Pattern pattern = Pattern.compile(regEx);
	      Matcher m = pattern.matcher(test);
	      
	     while( m.find() ){
	   //   System.out.println("Parentheses found at Start: "+m.start());
	      textBone.add(m.start());
	     }
	     
	     int[][] pairs = new int[textBone.size()/2][2];
	     int count = 0;
	     int start = 0;
	     int end = 0;
	     int n = 0;
	    
	    for(int j = 0; j < textBone.size(); j++){
	      start = textBone.get(j);
	      if (textBone.get(j)==0)
	         continue;
	      else{      
	         int t = j;
	         do {
	             if (test.charAt(textBone.get(t))=='('||test.charAt(textBone.get(t))=='（'){
	                 count++;
	                 t++;
	              }
	              if (test.charAt(textBone.get(t))==')'||test.charAt(textBone.get(t))=='）'){
	                 count--;
	                 t++;
	              } 
	         }while(count!=0);
	         end = textBone.get(t-1);
	         textBone.set(t-1,0);
	         t++;
	         pairs[n][0] = start;  //½«Åä¶ÔµÄ½á¹ûÐ´Èë¶þÎ»Êý×é
	         pairs[n][1] = end;
	         n++;
	      }
	   }
	  return pairs;
	}
	  
	
	  /*
	   * get the row number of str in the field of table
	   */
	    public static int getRowNum(Table table, String str, String field){
	    	//²âÊÔµã
	    	//result = 0; 
	    	int result = -1;
	    	if(str!=null){
		    	for(int i=0;i<table.getRowCount();i++){
		    		String com = table.getString(i, field);
		    		if(com.equals(str)){
		    			result = i;
		    			return result;
		    		}
		    		
		    	}
	    	}
	    	return result;
	    }
	    
	    public static Vector<Integer> getRowNumList(Table table, String str, String field){
	    	//²âÊÔµã
	    	//result = 0; 
	    	Vector<Integer> result = new Vector<Integer>(1,1);
	    	if(str!=null){
		    	for(int i=0;i<table.getRowCount();i++){
		    		String com = table.getString(i, field);
		    		if(com.equals(str)){
		    			result.add(i);
		    		}
		    		
		    	}
	    	}
	    	return result;
	    }
	    
	    public static int getRowNum(Table table, int str, String field){
	    	//²âÊÔµã
	    	//result = 0; 
	    	int result = -1;
	    	
	    	for(int i=0;i<table.getRowCount();i++){
	    		int com = table.getInt(i, field);
	    		if(com == str){
	    			result = i;
	    			return result;
	    		}
	    		
	    	}
	    	return result;
	    }
	    
	    /*
	     * have already deleted the white space
	     * output the string of a xml file by using xsl in the path of xslPath
	     */
	    public static String readXML(String resultPath, String xslPath, String outputPath){
	    	try {
				ui.Utility.transformation(resultPath,xslPath,outputPath, "text");
			} catch (SaxonApiException e) {
				// TODO Auto-generated catch block
				e.printStackTrace();
			}
			String s = null;
			
			try {
				s = ui.Utility.readFile(outputPath);
			} catch (IOException e) {
				// TODO Auto-generated catch block
				e.printStackTrace();
			}
			
			return Utility.deleteSpace(s);
			
	    }

	    public static String putIndent(int blank){
	        StringBuffer buf = new StringBuffer(10);
	        for(int i = 0; i < blank; i++){
	              	buf.append(constants.GTextbookConstants.Indent);
	              }
	        return buf.toString();
	        }
	    

		public static Node getChildByName(Node current, String nodeName, String mode){
			
			Node result = null;
			boolean flag = false;
			int count = 100;
			if(current != null){
			NodeList list = current.getChildNodes();
			if(list.getLength()>0){
				for(int i = 0; i < list.getLength(); i++){
					if(list.item(i).getNodeName().equals(nodeName)){
						result = list.item(i);
						flag = true;
						//System.out.println("mark" + i);
						break;
					}				
				}
				
				if(!mode.equals("*")){
					count = Integer.parseInt(mode)-1;
				}
			
				if(flag == false && count!=0){
					for(int j = 0; j < list.getLength(); j++){
						   //System.out.println("sss" + j);
						   result = getChildByName(list.item(j),nodeName, mode);
						   if(result != null){
							   break;
						   }
						}				
					}
			}	
			}
			return result;
		}
		
		/*
		 * id is counted from 1 
		 */
		public static Node getChildById(Node current, int id, short type){
			
			Node result = null;
			if(current != null){
			NodeList list = current.getChildNodes();
			int count = 0;
			if(list.getLength()>0){
				for(int i = 0; i < list.getLength(); i++){
					if(list.item(i).getNodeType()== type){
						count++;
						if(count == id){
							result = list.item(i);
							break;
						}
					}
				}
			}
			}
			return result; 

		}
		
		public static String getAttr(Node current, String AttrName){
			String result = null;
			short type = current.getNodeType();
			if(type == ELEMENT_NODE){
				if(((Element)current).hasAttribute(AttrName)){
					NamedNodeMap attrs = current.getAttributes();
					Attr attr = (Attr)attrs.getNamedItem(AttrName);
					result = attr.getValue();
				}
			}
			return result;
		}
		
		//return the number of the children with name for an element node
		public static int countElementChild(Node node, String name){
			int  result = 0;
			if(node != null && node.getNodeType() == ELEMENT_NODE){
				NodeList children = node.getChildNodes();
				for(int j = 0; j < children.getLength(); j++){
					short innerType = children.item(j).getNodeType();
					if(innerType == ELEMENT_NODE){
						if(children.item(j).getNodeName().equals(name)||name.equals("*")){
							result++;
						}					
					}
				}
			}	
			return result;
		}
		
		public static boolean isInStringArray(String str, ArrayList<String> list){
			boolean result = false;
			for(int i = 0; i < list.size(); i++){
				if(str.indexOf(list.get(i))==0){
					result = true;
					break;
				}
			}
			return result;
		}
		
		public static Vector<Type> deleteRedundant(Vector<Type> list){
			Vector<Type> result = new Vector<Type>(1,1);
			boolean flag = false;
			if(list.size()>0){
				result.add(list.get(0));     // ³õÊ¼»¯
				for(int i = 0; i < list.size();i++){
					flag = false;
					for(int j = 0; j < result.size(); j++){
						if(list.get(i).getValue().equals(result.get(j).getValue())){
							flag = true;
							break;
						}
					}
					if(flag == false){
						result.add(list.get(i));
					}
				}
			}
			
			return result;
		}
		
		
		public static Vector<Integer> generateRandomDiffSet(int count, int size){
			Vector<Integer> result = new Vector<Integer>(1,1);
			Random rs = new Random();   
			
			while(true){
				int buf = Math.abs(rs.nextInt()%size);
				//System.out.println(buf);
				if(result.size()==0){
					result.add(buf+1);
				}else
					if(result.size()==count){
						break;
					}else{
						boolean flag = true;
						for(int i = 0 ; i < result.size(); i++){
							if(buf + 1 ==result.get(i)){
								flag = false;
								break;
							}
						}
						if(flag == true){
							result.add(buf+1);
						}
					}
				
				
			}
			
			return result;
		}
		
		

		public static boolean matchReservedWords(String pattern, ArrayList<String> array){
			boolean result = false;
			for(int i = 0; i < array.size();i++){
				if(pattern.indexOf(array.get(i)+"(")==0){
					result = true;
					break;
					
				}
			}
			return result;
		}
		
		public static void print(Table table){
			for(int i = 0; i < table.getRowCount(); i++){
				for(int j = 0; j < table.getColumnCount(); j++){
					if(table.get(i, j)!=null){
						System.out.print(table.get(i, j).toString()+"----");
					}else{
						System.out.print("null----");
					}
				}
				System.out.print("\n");
			}
		}
		
		public static String formalize(String text, WebBrowser CoreNLPBrowser, JFrame CoreNLPFrame){
			File tempPath = new File(constants.GTextbookConstants.TEMP_NLP_PATH+"/sandbox.txt");
			ui.Utility.saveFile(null, text, tempPath);
			return formalize(tempPath,CoreNLPBrowser,CoreNLPFrame);
		}
		
		
		public static String formalize(File sourceFilePath, WebBrowser CoreNLPBrowser, JFrame CoreNLPFrame){
			//generate the CoreNLP XML output by using CoreNLP
			//replace the concepts in the statements 
			if(sourceFilePath!=null){
				String content = "Read file content error!";
				int conclusionSize = 0;
				int hypothesisSize = 0;
				String CoreNLPXMLoutputPath = null;
				try {
					content = ui.Utility.readFile(sourceFilePath.getPath());
					Corpus.initialize();
					for(Iterator iter=Corpus.functionMap.entrySet().iterator(); iter.hasNext();){  
					    Entry entry = (Entry)iter.next();  
					    content = content.replaceAll((String)entry.getKey(), (String)entry.getValue()); 
					    System.out.println(entry.getKey()+":"+entry.getValue());
					} 
					
				} catch (IOException e2) {
					// TODO Auto-generated catch block
					e2.printStackTrace();
				}
				
				
				//analyze the content of the input file and out put hypothesis and conclusion
				int endIndex = content.indexOf("Then");
				if(endIndex == -1){
					Vector<String> Csentences = ui.Utility.getItemsBySeparator(content.trim(),".");
					conclusionSize = Csentences.size();
				}else{
	        		String hypothesis = content.substring(0,endIndex);
	        		Vector<String> Hsentences = ui.Utility.getItemsBySeparator(hypothesis.trim(),".");
	        		hypothesisSize = Hsentences.size();
	        		String conclusion = content.substring(endIndex+5,content.length());
	        		Vector<String> Csentences = ui.Utility.getItemsBySeparator(conclusion.trim(),".");
	        		conclusionSize = Csentences.size();
	        	}
				
				//System.out.println(hypothesisSize + ":" + conclusionSize);
				
				//remove the extra key words
				content = content.replaceAll("If", "").replaceAll("Then", "");
				

				String NLTempFile = constants.GTextbookConstants.TEMP_NLP_PATH + 
							sourceFilePath.getPath().substring(sourceFilePath.getPath().replaceAll("\\\\", "/").lastIndexOf("/"),sourceFilePath.getPath().lastIndexOf(".txt"))+"_temp.txt";
				
			
				ui.Utility.saveFile(null, content, new File(NLTempFile));
				
				// TODO use CourNLP to generate CoreNLPXMLoutput in XML
				
				//open the CoreNLP XML output of the input NLtarget text file
				try {
					CoreNLPXMLoutputPath = NLTempFile+".xml";
					CoreNLPBrowser.setURL(new URL("file:///"+CoreNLPXMLoutputPath));
					CoreNLPFrame.setTitle("CoreNLP analytic output - " + CoreNLPXMLoutputPath);
					CoreNLPFrame.setVisible(true);
					
				} catch (MalformedURLException e1) {
					// TODO Auto-generated catch block
					e1.printStackTrace();
				}
				
				
				//transform NL into GDL
				
				//String CoreNLPXMLoutputPath = NLTempFile+".xml";
	    		String s = sourceFilePath.getPath().replaceAll("\\\\", "/");
			    String name = s.substring(s.lastIndexOf("/")+1, s.lastIndexOf(".")).trim();
			    String targetPath = constants.GTextbookConstants.TEMP_NLP_FORMAL_PATH + "\\"+name+".txt";
	    		
	    		 /* NLP formalization process
	    		  * input  : CoreNLPXMLoutputPath
	    		  * output : target
	    		  */
	    		
	    		StringBuffer assume = new StringBuffer();
	    		StringBuffer show = new StringBuffer();
	    		assume.append("assume(");
	    		show.append("show(");
	    	
	    		if(CoreNLPXMLoutputPath !=null && new File(CoreNLPXMLoutputPath).exists()){
		    		Corpus corpus = new Corpus(CoreNLPXMLoutputPath);
		    		
		    		if(corpus.tokens.size()==hypothesisSize+conclusionSize){
		        		
		    			for(int i = 0; i < hypothesisSize; i++){
		        			Table tokens = corpus.tokens.get(i);
		        			System.out.println("*********tokens*********");
		        			automatica.Utility.print(tokens);
		        			System.out.println("************************");
		        			Table relations = corpus.relations.get(i);
		        			System.out.println("*********relations*********");
		        			automatica.Utility.print(relations);
		        			System.out.println("***************************");
		        			Table variables = corpus.variables.get(i);
		        			PhraseParser p = new PhraseParser(tokens,relations,variables,corpus.coreference,i+1);
		        			System.out.println("sentence: " + i);
		        			String result = p.work();
		        			System.out.println(result);
		        			System.out.println("*********variables*********");
		        			automatica.Utility.print(variables);
		        			System.out.println("***************************");
		        			System.out.println("*********coreference*********");
		        			automatica.Utility.print(corpus.coreference);
		        			System.out.println("***************************");    
		        			for(int j = variables.getRowCount()-1; j >=0 ; j--){
		        				if(variables.getString(j, "type").equals("Point")){
		        					assume.append(variables.getString(j, "name")+":=point(),");
		        				}
		        			}
		        			assume.append(result+",");
		        			
		        		}
		        		
		        		for(int i = hypothesisSize; i < corpus.tokens.size(); i++){
		        			Table tokens = corpus.tokens.get(i);
		        			System.out.println("*********tokens*********");
		        			automatica.Utility.print(tokens);
		        			System.out.println("************************");
		        			Table relations = corpus.relations.get(i);
		        			System.out.println("*********relations*********");
		        			automatica.Utility.print(relations);
		        			System.out.println("***************************");
		        			Table variables = corpus.variables.get(i);
		        			PhraseParser p = new PhraseParser(tokens,relations,variables, corpus.coreference,i+1);
		        			String result = p.work();
		        			System.out.println("*********variables*********");
		        			automatica.Utility.print(variables);
		        			System.out.println("***************************");
		        			System.out.println("*********coreference*********");
		        			automatica.Utility.print(corpus.coreference);
		        			System.out.println("***************************");
		        			show.append(result+",");
		        			for(int j = 0; j < variables.getRowCount(); j++){
		        				if(variables.getString(j, "type").equals("Point")){
		        					assume.append(variables.getString(j, "name")+":=point(),");
		        				}
		        			}
		        		}
		        		if(show.lastIndexOf(",")!=-1){
		        			show.replace(show.lastIndexOf(","), show.length(), ")");
		        		}else{
		        			show.append(")");
		        		}
		        		
		        		if(assume.lastIndexOf(",")!=-1){
		        			assume.replace(assume.lastIndexOf(","), assume.length(), ")");
		        		}else{
		        			assume.append(")");
		        		}
		        		//construct the output string and save the string into target
			    		String formalizationResult = "Theorem("+ name +",Theorem,"+assume+","+show+")";
			    		ui.Utility.saveFile(null, formalizationResult, new File(targetPath));
			    		return targetPath;
		        		
		    		}else{
		    			JOptionPane.showMessageDialog(null,
		                        "Please check your input natural statemnts!",
		                        "Identify hypothesis and conclusion error", JOptionPane.ERROR_MESSAGE);
		    			 return "";
		    		}
		    		
		    		
	    		}else{
	    			JOptionPane.showMessageDialog(null, "There is no CoreNLP analytic output XML file!", "Warning", JOptionPane.WARNING_MESSAGE);
					return "";
	    		}
			}else{
				JOptionPane.showMessageDialog(null, "Please select a problem file!", "Warning", JOptionPane.WARNING_MESSAGE);
				return null;
			}
			
			
		}
		
		public static DirectedGraph<Integer, DefaultEdge> prefuseGraph2JGraphT(Graph graph, String preField, String subField)
	    {
	        DirectedGraph<Integer, DefaultEdge> result =
	            new DefaultDirectedGraph<Integer, DefaultEdge>(DefaultEdge.class);
	        if(graph!=null){
	        	Table nodes = graph.getNodeTable();
	        
	        	// add the vertices
	        	for(int i = 0; i < nodes.getRowCount(); i++){
	        		result.addVertex(i);
	        	}

	        	Table edges = graph.getEdgeTable();
	        
	        	// add edges to create linking structure
	        	for(int j = 0; j < edges.getRowCount(); j++){
	        		result.addEdge(edges.getInt(j, preField), edges.getInt(j, subField));
	        	}
	        }

	        return result;
	    }
		
		public static boolean isDAG(Graph prefuseGraph){
			DirectedGraph<Integer, DefaultEdge> g = prefuseGraph2JGraphT(prefuseGraph,"pre","sub");
			CycleDetector cycleDetector = new CycleDetector(g);
			return !cycleDetector.detectCycles();
		}
	  
}

